Left Termination proof of /tmp/tmp3JNbTo/t.pl

Left Termination of the query pattern t(b) w.r.t. the given Prolog program could successfully be proven:

↳ PROLOG

  ↳ PrologToPiTRSProof

t₁(N) :- ll₂(N, Xs), select₃(underscore, Xs, Xs1), ll₂(M, Xs1), t₁(M).
t₁(0₀).
ll₂(s₁(N), .₂(X, Xs)) :- ll₂(N, Xs).
ll₂(0₀, {}₀).
select₃(X, .₂(Y, Xs), .₂(Y, Ys)) :- select₃(X, Xs, Ys).
select₃(X, .₂(X, Xs), Xs).

With regard to the inferred argument filtering the predicates were used in the following modes:
t₁: (b)
ll₂: (b,f) (f,b)
select₃: (f,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

t_1_in_g₁(N) -> if_t_1_in_1_g₂(N, ll_2_in_ga₂(N, Xs))
ll_2_in_ga₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ga₄(N, X, Xs, ll_2_in_ga₂(N, Xs))
ll_2_in_ga₂(0_0, []_0) -> ll_2_out_ga₂(0_0, []_0)
if_ll_2_in_1_ga₄(N, X, Xs, ll_2_out_ga₂(N, Xs)) -> ll_2_out_ga₂(s_1₁(N), ._2₂(X, Xs))
if_t_1_in_1_g₂(N, ll_2_out_ga₂(N, Xs)) -> if_t_1_in_2_g₃(N, Xs, select_3_in_aga₃(underscore, Xs, Xs1))
select_3_in_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys)) -> if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_in_aga₃(X, Xs, Ys))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_out_aga₃(X, Xs, Ys)) -> select_3_out_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys))
if_t_1_in_2_g₃(N, Xs, select_3_out_aga₃(underscore, Xs, Xs1)) -> if_t_1_in_3_g₃(N, Xs1, ll_2_in_ag₂(M, Xs1))
ll_2_in_ag₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ag₄(N, X, Xs, ll_2_in_ag₂(N, Xs))
ll_2_in_ag₂(0_0, []_0) -> ll_2_out_ag₂(0_0, []_0)
if_ll_2_in_1_ag₄(N, X, Xs, ll_2_out_ag₂(N, Xs)) -> ll_2_out_ag₂(s_1₁(N), ._2₂(X, Xs))
if_t_1_in_3_g₃(N, Xs1, ll_2_out_ag₂(M, Xs1)) -> if_t_1_in_4_g₃(N, M, t_1_in_g₁(M))
t_1_in_g₁(0_0) -> t_1_out_g₁(0_0)
if_t_1_in_4_g₃(N, M, t_1_out_g₁(M)) -> t_1_out_g₁(N)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

t_1_in_g₁(N) -> if_t_1_in_1_g₂(N, ll_2_in_ga₂(N, Xs))
ll_2_in_ga₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ga₄(N, X, Xs, ll_2_in_ga₂(N, Xs))
ll_2_in_ga₂(0_0, []_0) -> ll_2_out_ga₂(0_0, []_0)
if_ll_2_in_1_ga₄(N, X, Xs, ll_2_out_ga₂(N, Xs)) -> ll_2_out_ga₂(s_1₁(N), ._2₂(X, Xs))
if_t_1_in_1_g₂(N, ll_2_out_ga₂(N, Xs)) -> if_t_1_in_2_g₃(N, Xs, select_3_in_aga₃(underscore, Xs, Xs1))
select_3_in_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys)) -> if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_in_aga₃(X, Xs, Ys))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_out_aga₃(X, Xs, Ys)) -> select_3_out_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys))
if_t_1_in_2_g₃(N, Xs, select_3_out_aga₃(underscore, Xs, Xs1)) -> if_t_1_in_3_g₃(N, Xs1, ll_2_in_ag₂(M, Xs1))
ll_2_in_ag₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ag₄(N, X, Xs, ll_2_in_ag₂(N, Xs))
ll_2_in_ag₂(0_0, []_0) -> ll_2_out_ag₂(0_0, []_0)
if_ll_2_in_1_ag₄(N, X, Xs, ll_2_out_ag₂(N, Xs)) -> ll_2_out_ag₂(s_1₁(N), ._2₂(X, Xs))
if_t_1_in_3_g₃(N, Xs1, ll_2_out_ag₂(M, Xs1)) -> if_t_1_in_4_g₃(N, M, t_1_in_g₁(M))
t_1_in_g₁(0_0) -> t_1_out_g₁(0_0)
if_t_1_in_4_g₃(N, M, t_1_out_g₁(M)) -> t_1_out_g₁(N)

T_1_IN_G₁(N) -> IF_T_1_IN_1_G₂(N, ll_2_in_ga₂(N, Xs))
T_1_IN_G₁(N) -> LL_2_IN_GA₂(N, Xs)
LL_2_IN_GA₂(s_1₁(N), ._2₂(X, Xs)) -> IF_LL_2_IN_1_GA₄(N, X, Xs, ll_2_in_ga₂(N, Xs))
LL_2_IN_GA₂(s_1₁(N), ._2₂(X, Xs)) -> LL_2_IN_GA₂(N, Xs)
IF_T_1_IN_1_G₂(N, ll_2_out_ga₂(N, Xs)) -> IF_T_1_IN_2_G₃(N, Xs, select_3_in_aga₃(underscore, Xs, Xs1))
IF_T_1_IN_1_G₂(N, ll_2_out_ga₂(N, Xs)) -> SELECT_3_IN_AGA₃(underscore, Xs, Xs1)
SELECT_3_IN_AGA₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys)) -> IF_SELECT_3_IN_1_AGA₅(X, Y, Xs, Ys, select_3_in_aga₃(X, Xs, Ys))
SELECT_3_IN_AGA₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys)) -> SELECT_3_IN_AGA₃(X, Xs, Ys)
IF_T_1_IN_2_G₃(N, Xs, select_3_out_aga₃(underscore, Xs, Xs1)) -> IF_T_1_IN_3_G₃(N, Xs1, ll_2_in_ag₂(M, Xs1))
IF_T_1_IN_2_G₃(N, Xs, select_3_out_aga₃(underscore, Xs, Xs1)) -> LL_2_IN_AG₂(M, Xs1)
LL_2_IN_AG₂(s_1₁(N), ._2₂(X, Xs)) -> IF_LL_2_IN_1_AG₄(N, X, Xs, ll_2_in_ag₂(N, Xs))
LL_2_IN_AG₂(s_1₁(N), ._2₂(X, Xs)) -> LL_2_IN_AG₂(N, Xs)
IF_T_1_IN_3_G₃(N, Xs1, ll_2_out_ag₂(M, Xs1)) -> IF_T_1_IN_4_G₃(N, M, t_1_in_g₁(M))
IF_T_1_IN_3_G₃(N, Xs1, ll_2_out_ag₂(M, Xs1)) -> T_1_IN_G₁(M)

The TRS R consists of the following rules:

t_1_in_g₁(N) -> if_t_1_in_1_g₂(N, ll_2_in_ga₂(N, Xs))
ll_2_in_ga₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ga₄(N, X, Xs, ll_2_in_ga₂(N, Xs))
ll_2_in_ga₂(0_0, []_0) -> ll_2_out_ga₂(0_0, []_0)
if_ll_2_in_1_ga₄(N, X, Xs, ll_2_out_ga₂(N, Xs)) -> ll_2_out_ga₂(s_1₁(N), ._2₂(X, Xs))
if_t_1_in_1_g₂(N, ll_2_out_ga₂(N, Xs)) -> if_t_1_in_2_g₃(N, Xs, select_3_in_aga₃(underscore, Xs, Xs1))
select_3_in_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys)) -> if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_in_aga₃(X, Xs, Ys))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_out_aga₃(X, Xs, Ys)) -> select_3_out_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys))
if_t_1_in_2_g₃(N, Xs, select_3_out_aga₃(underscore, Xs, Xs1)) -> if_t_1_in_3_g₃(N, Xs1, ll_2_in_ag₂(M, Xs1))
ll_2_in_ag₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ag₄(N, X, Xs, ll_2_in_ag₂(N, Xs))
ll_2_in_ag₂(0_0, []_0) -> ll_2_out_ag₂(0_0, []_0)
if_ll_2_in_1_ag₄(N, X, Xs, ll_2_out_ag₂(N, Xs)) -> ll_2_out_ag₂(s_1₁(N), ._2₂(X, Xs))
if_t_1_in_3_g₃(N, Xs1, ll_2_out_ag₂(M, Xs1)) -> if_t_1_in_4_g₃(N, M, t_1_in_g₁(M))
t_1_in_g₁(0_0) -> t_1_out_g₁(0_0)
if_t_1_in_4_g₃(N, M, t_1_out_g₁(M)) -> t_1_out_g₁(N)

The argument filtering Pi contains the following mapping:
t_1_in_g₁(x1) = t_1_in_g₁(x1)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
._2₂(x1, x2) = ._2₁(x2)
[]_0 = []_0
if_t_1_in_1_g₂(x1, x2) = if_t_1_in_1_g₁(x2)
ll_2_in_ga₂(x1, x2) = ll_2_in_ga₁(x1)
if_ll_2_in_1_ga₄(x1, x2, x3, x4) = if_ll_2_in_1_ga₁(x4)
ll_2_out_ga₂(x1, x2) = ll_2_out_ga₁(x2)
if_t_1_in_2_g₃(x1, x2, x3) = if_t_1_in_2_g₁(x3)
select_3_in_aga₃(x1, x2, x3) = select_3_in_aga₁(x2)
if_select_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_select_3_in_1_aga₁(x5)
select_3_out_aga₃(x1, x2, x3) = select_3_out_aga₁(x3)
if_t_1_in_3_g₃(x1, x2, x3) = if_t_1_in_3_g₁(x3)
ll_2_in_ag₂(x1, x2) = ll_2_in_ag₁(x2)
if_ll_2_in_1_ag₄(x1, x2, x3, x4) = if_ll_2_in_1_ag₁(x4)
ll_2_out_ag₂(x1, x2) = ll_2_out_ag₁(x1)
if_t_1_in_4_g₃(x1, x2, x3) = if_t_1_in_4_g₁(x3)
t_1_out_g₁(x1) = t_1_out_g
IF_LL_2_IN_1_AG₄(x1, x2, x3, x4) = IF_LL_2_IN_1_AG₁(x4)
IF_T_1_IN_1_G₂(x1, x2) = IF_T_1_IN_1_G₁(x2)
LL_2_IN_AG₂(x1, x2) = LL_2_IN_AG₁(x2)
IF_LL_2_IN_1_GA₄(x1, x2, x3, x4) = IF_LL_2_IN_1_GA₁(x4)
IF_T_1_IN_4_G₃(x1, x2, x3) = IF_T_1_IN_4_G₁(x3)
IF_T_1_IN_3_G₃(x1, x2, x3) = IF_T_1_IN_3_G₁(x3)
IF_T_1_IN_2_G₃(x1, x2, x3) = IF_T_1_IN_2_G₁(x3)
SELECT_3_IN_AGA₃(x1, x2, x3) = SELECT_3_IN_AGA₁(x2)
IF_SELECT_3_IN_1_AGA₅(x1, x2, x3, x4, x5) = IF_SELECT_3_IN_1_AGA₁(x5)
T_1_IN_G₁(x1) = T_1_IN_G₁(x1)
LL_2_IN_GA₂(x1, x2) = LL_2_IN_GA₁(x1)

We have to consider all (P,R,Pi)-chains

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

T_1_IN_G₁(N) -> IF_T_1_IN_1_G₂(N, ll_2_in_ga₂(N, Xs))
T_1_IN_G₁(N) -> LL_2_IN_GA₂(N, Xs)
LL_2_IN_GA₂(s_1₁(N), ._2₂(X, Xs)) -> IF_LL_2_IN_1_GA₄(N, X, Xs, ll_2_in_ga₂(N, Xs))
LL_2_IN_GA₂(s_1₁(N), ._2₂(X, Xs)) -> LL_2_IN_GA₂(N, Xs)
IF_T_1_IN_1_G₂(N, ll_2_out_ga₂(N, Xs)) -> IF_T_1_IN_2_G₃(N, Xs, select_3_in_aga₃(underscore, Xs, Xs1))
IF_T_1_IN_1_G₂(N, ll_2_out_ga₂(N, Xs)) -> SELECT_3_IN_AGA₃(underscore, Xs, Xs1)
SELECT_3_IN_AGA₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys)) -> IF_SELECT_3_IN_1_AGA₅(X, Y, Xs, Ys, select_3_in_aga₃(X, Xs, Ys))
SELECT_3_IN_AGA₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys)) -> SELECT_3_IN_AGA₃(X, Xs, Ys)
IF_T_1_IN_2_G₃(N, Xs, select_3_out_aga₃(underscore, Xs, Xs1)) -> IF_T_1_IN_3_G₃(N, Xs1, ll_2_in_ag₂(M, Xs1))
IF_T_1_IN_2_G₃(N, Xs, select_3_out_aga₃(underscore, Xs, Xs1)) -> LL_2_IN_AG₂(M, Xs1)
LL_2_IN_AG₂(s_1₁(N), ._2₂(X, Xs)) -> IF_LL_2_IN_1_AG₄(N, X, Xs, ll_2_in_ag₂(N, Xs))
LL_2_IN_AG₂(s_1₁(N), ._2₂(X, Xs)) -> LL_2_IN_AG₂(N, Xs)
IF_T_1_IN_3_G₃(N, Xs1, ll_2_out_ag₂(M, Xs1)) -> IF_T_1_IN_4_G₃(N, M, t_1_in_g₁(M))
IF_T_1_IN_3_G₃(N, Xs1, ll_2_out_ag₂(M, Xs1)) -> T_1_IN_G₁(M)

The TRS R consists of the following rules:

t_1_in_g₁(N) -> if_t_1_in_1_g₂(N, ll_2_in_ga₂(N, Xs))
ll_2_in_ga₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ga₄(N, X, Xs, ll_2_in_ga₂(N, Xs))
ll_2_in_ga₂(0_0, []_0) -> ll_2_out_ga₂(0_0, []_0)
if_ll_2_in_1_ga₄(N, X, Xs, ll_2_out_ga₂(N, Xs)) -> ll_2_out_ga₂(s_1₁(N), ._2₂(X, Xs))
if_t_1_in_1_g₂(N, ll_2_out_ga₂(N, Xs)) -> if_t_1_in_2_g₃(N, Xs, select_3_in_aga₃(underscore, Xs, Xs1))
select_3_in_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys)) -> if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_in_aga₃(X, Xs, Ys))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_out_aga₃(X, Xs, Ys)) -> select_3_out_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys))
if_t_1_in_2_g₃(N, Xs, select_3_out_aga₃(underscore, Xs, Xs1)) -> if_t_1_in_3_g₃(N, Xs1, ll_2_in_ag₂(M, Xs1))
ll_2_in_ag₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ag₄(N, X, Xs, ll_2_in_ag₂(N, Xs))
ll_2_in_ag₂(0_0, []_0) -> ll_2_out_ag₂(0_0, []_0)
if_ll_2_in_1_ag₄(N, X, Xs, ll_2_out_ag₂(N, Xs)) -> ll_2_out_ag₂(s_1₁(N), ._2₂(X, Xs))
if_t_1_in_3_g₃(N, Xs1, ll_2_out_ag₂(M, Xs1)) -> if_t_1_in_4_g₃(N, M, t_1_in_g₁(M))
t_1_in_g₁(0_0) -> t_1_out_g₁(0_0)
if_t_1_in_4_g₃(N, M, t_1_out_g₁(M)) -> t_1_out_g₁(N)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

LL_2_IN_AG₂(s_1₁(N), ._2₂(X, Xs)) -> LL_2_IN_AG₂(N, Xs)

The TRS R consists of the following rules:

t_1_in_g₁(N) -> if_t_1_in_1_g₂(N, ll_2_in_ga₂(N, Xs))
ll_2_in_ga₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ga₄(N, X, Xs, ll_2_in_ga₂(N, Xs))
ll_2_in_ga₂(0_0, []_0) -> ll_2_out_ga₂(0_0, []_0)
if_ll_2_in_1_ga₄(N, X, Xs, ll_2_out_ga₂(N, Xs)) -> ll_2_out_ga₂(s_1₁(N), ._2₂(X, Xs))
if_t_1_in_1_g₂(N, ll_2_out_ga₂(N, Xs)) -> if_t_1_in_2_g₃(N, Xs, select_3_in_aga₃(underscore, Xs, Xs1))
select_3_in_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys)) -> if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_in_aga₃(X, Xs, Ys))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_out_aga₃(X, Xs, Ys)) -> select_3_out_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys))
if_t_1_in_2_g₃(N, Xs, select_3_out_aga₃(underscore, Xs, Xs1)) -> if_t_1_in_3_g₃(N, Xs1, ll_2_in_ag₂(M, Xs1))
ll_2_in_ag₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ag₄(N, X, Xs, ll_2_in_ag₂(N, Xs))
ll_2_in_ag₂(0_0, []_0) -> ll_2_out_ag₂(0_0, []_0)
if_ll_2_in_1_ag₄(N, X, Xs, ll_2_out_ag₂(N, Xs)) -> ll_2_out_ag₂(s_1₁(N), ._2₂(X, Xs))
if_t_1_in_3_g₃(N, Xs1, ll_2_out_ag₂(M, Xs1)) -> if_t_1_in_4_g₃(N, M, t_1_in_g₁(M))
t_1_in_g₁(0_0) -> t_1_out_g₁(0_0)
if_t_1_in_4_g₃(N, M, t_1_out_g₁(M)) -> t_1_out_g₁(N)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

LL_2_IN_AG₂(s_1₁(N), ._2₂(X, Xs)) -> LL_2_IN_AG₂(N, Xs)

R is empty.
The argument filtering Pi contains the following mapping:
s_1₁(x1) = s_1₁(x1)
._2₂(x1, x2) = ._2₁(x2)
LL_2_IN_AG₂(x1, x2) = LL_2_IN_AG₁(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

LL_2_IN_AG₁(._2₁(Xs)) -> LL_2_IN_AG₁(Xs)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {LL_2_IN_AG₁}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

LL_2_IN_AG₁(._2₁(Xs)) -> LL_2_IN_AG₁(Xs)
The graph contains the following edges 1 > 1

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SELECT_3_IN_AGA₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys)) -> SELECT_3_IN_AGA₃(X, Xs, Ys)

The TRS R consists of the following rules:

t_1_in_g₁(N) -> if_t_1_in_1_g₂(N, ll_2_in_ga₂(N, Xs))
ll_2_in_ga₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ga₄(N, X, Xs, ll_2_in_ga₂(N, Xs))
ll_2_in_ga₂(0_0, []_0) -> ll_2_out_ga₂(0_0, []_0)
if_ll_2_in_1_ga₄(N, X, Xs, ll_2_out_ga₂(N, Xs)) -> ll_2_out_ga₂(s_1₁(N), ._2₂(X, Xs))
if_t_1_in_1_g₂(N, ll_2_out_ga₂(N, Xs)) -> if_t_1_in_2_g₃(N, Xs, select_3_in_aga₃(underscore, Xs, Xs1))
select_3_in_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys)) -> if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_in_aga₃(X, Xs, Ys))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_out_aga₃(X, Xs, Ys)) -> select_3_out_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys))
if_t_1_in_2_g₃(N, Xs, select_3_out_aga₃(underscore, Xs, Xs1)) -> if_t_1_in_3_g₃(N, Xs1, ll_2_in_ag₂(M, Xs1))
ll_2_in_ag₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ag₄(N, X, Xs, ll_2_in_ag₂(N, Xs))
ll_2_in_ag₂(0_0, []_0) -> ll_2_out_ag₂(0_0, []_0)
if_ll_2_in_1_ag₄(N, X, Xs, ll_2_out_ag₂(N, Xs)) -> ll_2_out_ag₂(s_1₁(N), ._2₂(X, Xs))
if_t_1_in_3_g₃(N, Xs1, ll_2_out_ag₂(M, Xs1)) -> if_t_1_in_4_g₃(N, M, t_1_in_g₁(M))
t_1_in_g₁(0_0) -> t_1_out_g₁(0_0)
if_t_1_in_4_g₃(N, M, t_1_out_g₁(M)) -> t_1_out_g₁(N)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SELECT_3_IN_AGA₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys)) -> SELECT_3_IN_AGA₃(X, Xs, Ys)

R is empty.
The argument filtering Pi contains the following mapping:
._2₂(x1, x2) = ._2₁(x2)
SELECT_3_IN_AGA₃(x1, x2, x3) = SELECT_3_IN_AGA₁(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

SELECT_3_IN_AGA₁(._2₁(Xs)) -> SELECT_3_IN_AGA₁(Xs)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {SELECT_3_IN_AGA₁}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

SELECT_3_IN_AGA₁(._2₁(Xs)) -> SELECT_3_IN_AGA₁(Xs)
The graph contains the following edges 1 > 1

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

LL_2_IN_GA₂(s_1₁(N), ._2₂(X, Xs)) -> LL_2_IN_GA₂(N, Xs)

The TRS R consists of the following rules:

t_1_in_g₁(N) -> if_t_1_in_1_g₂(N, ll_2_in_ga₂(N, Xs))
ll_2_in_ga₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ga₄(N, X, Xs, ll_2_in_ga₂(N, Xs))
ll_2_in_ga₂(0_0, []_0) -> ll_2_out_ga₂(0_0, []_0)
if_ll_2_in_1_ga₄(N, X, Xs, ll_2_out_ga₂(N, Xs)) -> ll_2_out_ga₂(s_1₁(N), ._2₂(X, Xs))
if_t_1_in_1_g₂(N, ll_2_out_ga₂(N, Xs)) -> if_t_1_in_2_g₃(N, Xs, select_3_in_aga₃(underscore, Xs, Xs1))
select_3_in_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys)) -> if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_in_aga₃(X, Xs, Ys))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_out_aga₃(X, Xs, Ys)) -> select_3_out_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys))
if_t_1_in_2_g₃(N, Xs, select_3_out_aga₃(underscore, Xs, Xs1)) -> if_t_1_in_3_g₃(N, Xs1, ll_2_in_ag₂(M, Xs1))
ll_2_in_ag₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ag₄(N, X, Xs, ll_2_in_ag₂(N, Xs))
ll_2_in_ag₂(0_0, []_0) -> ll_2_out_ag₂(0_0, []_0)
if_ll_2_in_1_ag₄(N, X, Xs, ll_2_out_ag₂(N, Xs)) -> ll_2_out_ag₂(s_1₁(N), ._2₂(X, Xs))
if_t_1_in_3_g₃(N, Xs1, ll_2_out_ag₂(M, Xs1)) -> if_t_1_in_4_g₃(N, M, t_1_in_g₁(M))
t_1_in_g₁(0_0) -> t_1_out_g₁(0_0)
if_t_1_in_4_g₃(N, M, t_1_out_g₁(M)) -> t_1_out_g₁(N)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

LL_2_IN_GA₂(s_1₁(N), ._2₂(X, Xs)) -> LL_2_IN_GA₂(N, Xs)

R is empty.
The argument filtering Pi contains the following mapping:
s_1₁(x1) = s_1₁(x1)
._2₂(x1, x2) = ._2₁(x2)
LL_2_IN_GA₂(x1, x2) = LL_2_IN_GA₁(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

LL_2_IN_GA₁(s_1₁(N)) -> LL_2_IN_GA₁(N)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {LL_2_IN_GA₁}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

LL_2_IN_GA₁(s_1₁(N)) -> LL_2_IN_GA₁(N)
The graph contains the following edges 1 > 1

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

IF_T_1_IN_1_G₂(N, ll_2_out_ga₂(N, Xs)) -> IF_T_1_IN_2_G₃(N, Xs, select_3_in_aga₃(underscore, Xs, Xs1))
IF_T_1_IN_2_G₃(N, Xs, select_3_out_aga₃(underscore, Xs, Xs1)) -> IF_T_1_IN_3_G₃(N, Xs1, ll_2_in_ag₂(M, Xs1))
IF_T_1_IN_3_G₃(N, Xs1, ll_2_out_ag₂(M, Xs1)) -> T_1_IN_G₁(M)
T_1_IN_G₁(N) -> IF_T_1_IN_1_G₂(N, ll_2_in_ga₂(N, Xs))

The TRS R consists of the following rules:

t_1_in_g₁(N) -> if_t_1_in_1_g₂(N, ll_2_in_ga₂(N, Xs))
ll_2_in_ga₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ga₄(N, X, Xs, ll_2_in_ga₂(N, Xs))
ll_2_in_ga₂(0_0, []_0) -> ll_2_out_ga₂(0_0, []_0)
if_ll_2_in_1_ga₄(N, X, Xs, ll_2_out_ga₂(N, Xs)) -> ll_2_out_ga₂(s_1₁(N), ._2₂(X, Xs))
if_t_1_in_1_g₂(N, ll_2_out_ga₂(N, Xs)) -> if_t_1_in_2_g₃(N, Xs, select_3_in_aga₃(underscore, Xs, Xs1))
select_3_in_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys)) -> if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_in_aga₃(X, Xs, Ys))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_out_aga₃(X, Xs, Ys)) -> select_3_out_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys))
if_t_1_in_2_g₃(N, Xs, select_3_out_aga₃(underscore, Xs, Xs1)) -> if_t_1_in_3_g₃(N, Xs1, ll_2_in_ag₂(M, Xs1))
ll_2_in_ag₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ag₄(N, X, Xs, ll_2_in_ag₂(N, Xs))
ll_2_in_ag₂(0_0, []_0) -> ll_2_out_ag₂(0_0, []_0)
if_ll_2_in_1_ag₄(N, X, Xs, ll_2_out_ag₂(N, Xs)) -> ll_2_out_ag₂(s_1₁(N), ._2₂(X, Xs))
if_t_1_in_3_g₃(N, Xs1, ll_2_out_ag₂(M, Xs1)) -> if_t_1_in_4_g₃(N, M, t_1_in_g₁(M))
t_1_in_g₁(0_0) -> t_1_out_g₁(0_0)
if_t_1_in_4_g₃(N, M, t_1_out_g₁(M)) -> t_1_out_g₁(N)

The argument filtering Pi contains the following mapping:
t_1_in_g₁(x1) = t_1_in_g₁(x1)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
._2₂(x1, x2) = ._2₁(x2)
[]_0 = []_0
if_t_1_in_1_g₂(x1, x2) = if_t_1_in_1_g₁(x2)
ll_2_in_ga₂(x1, x2) = ll_2_in_ga₁(x1)
if_ll_2_in_1_ga₄(x1, x2, x3, x4) = if_ll_2_in_1_ga₁(x4)
ll_2_out_ga₂(x1, x2) = ll_2_out_ga₁(x2)
if_t_1_in_2_g₃(x1, x2, x3) = if_t_1_in_2_g₁(x3)
select_3_in_aga₃(x1, x2, x3) = select_3_in_aga₁(x2)
if_select_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_select_3_in_1_aga₁(x5)
select_3_out_aga₃(x1, x2, x3) = select_3_out_aga₁(x3)
if_t_1_in_3_g₃(x1, x2, x3) = if_t_1_in_3_g₁(x3)
ll_2_in_ag₂(x1, x2) = ll_2_in_ag₁(x2)
if_ll_2_in_1_ag₄(x1, x2, x3, x4) = if_ll_2_in_1_ag₁(x4)
ll_2_out_ag₂(x1, x2) = ll_2_out_ag₁(x1)
if_t_1_in_4_g₃(x1, x2, x3) = if_t_1_in_4_g₁(x3)
t_1_out_g₁(x1) = t_1_out_g
IF_T_1_IN_1_G₂(x1, x2) = IF_T_1_IN_1_G₁(x2)
IF_T_1_IN_3_G₃(x1, x2, x3) = IF_T_1_IN_3_G₁(x3)
IF_T_1_IN_2_G₃(x1, x2, x3) = IF_T_1_IN_2_G₁(x3)
T_1_IN_G₁(x1) = T_1_IN_G₁(x1)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

IF_T_1_IN_1_G₂(N, ll_2_out_ga₂(N, Xs)) -> IF_T_1_IN_2_G₃(N, Xs, select_3_in_aga₃(underscore, Xs, Xs1))
IF_T_1_IN_2_G₃(N, Xs, select_3_out_aga₃(underscore, Xs, Xs1)) -> IF_T_1_IN_3_G₃(N, Xs1, ll_2_in_ag₂(M, Xs1))
IF_T_1_IN_3_G₃(N, Xs1, ll_2_out_ag₂(M, Xs1)) -> T_1_IN_G₁(M)
T_1_IN_G₁(N) -> IF_T_1_IN_1_G₂(N, ll_2_in_ga₂(N, Xs))

The TRS R consists of the following rules:

select_3_in_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys)) -> if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_in_aga₃(X, Xs, Ys))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
ll_2_in_ag₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ag₄(N, X, Xs, ll_2_in_ag₂(N, Xs))
ll_2_in_ag₂(0_0, []_0) -> ll_2_out_ag₂(0_0, []_0)
ll_2_in_ga₂(s_1₁(N), ._2₂(X, Xs)) -> if_ll_2_in_1_ga₄(N, X, Xs, ll_2_in_ga₂(N, Xs))
ll_2_in_ga₂(0_0, []_0) -> ll_2_out_ga₂(0_0, []_0)
if_select_3_in_1_aga₅(X, Y, Xs, Ys, select_3_out_aga₃(X, Xs, Ys)) -> select_3_out_aga₃(X, ._2₂(Y, Xs), ._2₂(Y, Ys))
if_ll_2_in_1_ag₄(N, X, Xs, ll_2_out_ag₂(N, Xs)) -> ll_2_out_ag₂(s_1₁(N), ._2₂(X, Xs))
if_ll_2_in_1_ga₄(N, X, Xs, ll_2_out_ga₂(N, Xs)) -> ll_2_out_ga₂(s_1₁(N), ._2₂(X, Xs))

The argument filtering Pi contains the following mapping:
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
._2₂(x1, x2) = ._2₁(x2)
[]_0 = []_0
ll_2_in_ga₂(x1, x2) = ll_2_in_ga₁(x1)
if_ll_2_in_1_ga₄(x1, x2, x3, x4) = if_ll_2_in_1_ga₁(x4)
ll_2_out_ga₂(x1, x2) = ll_2_out_ga₁(x2)
select_3_in_aga₃(x1, x2, x3) = select_3_in_aga₁(x2)
if_select_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_select_3_in_1_aga₁(x5)
select_3_out_aga₃(x1, x2, x3) = select_3_out_aga₁(x3)
ll_2_in_ag₂(x1, x2) = ll_2_in_ag₁(x2)
if_ll_2_in_1_ag₄(x1, x2, x3, x4) = if_ll_2_in_1_ag₁(x4)
ll_2_out_ag₂(x1, x2) = ll_2_out_ag₁(x1)
IF_T_1_IN_1_G₂(x1, x2) = IF_T_1_IN_1_G₁(x2)
IF_T_1_IN_3_G₃(x1, x2, x3) = IF_T_1_IN_3_G₁(x3)
IF_T_1_IN_2_G₃(x1, x2, x3) = IF_T_1_IN_2_G₁(x3)
T_1_IN_G₁(x1) = T_1_IN_G₁(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPPoloProof

Q DP problem:
The TRS P consists of the following rules:

IF_T_1_IN_1_G₁(ll_2_out_ga₁(Xs)) -> IF_T_1_IN_2_G₁(select_3_in_aga₁(Xs))
IF_T_1_IN_2_G₁(select_3_out_aga₁(Xs1)) -> IF_T_1_IN_3_G₁(ll_2_in_ag₁(Xs1))
IF_T_1_IN_3_G₁(ll_2_out_ag₁(M)) -> T_1_IN_G₁(M)
T_1_IN_G₁(N) -> IF_T_1_IN_1_G₁(ll_2_in_ga₁(N))

The TRS R consists of the following rules:

select_3_in_aga₁(._2₁(Xs)) -> if_select_3_in_1_aga₁(select_3_in_aga₁(Xs))
select_3_in_aga₁(._2₁(Xs)) -> select_3_out_aga₁(Xs)
ll_2_in_ag₁(._2₁(Xs)) -> if_ll_2_in_1_ag₁(ll_2_in_ag₁(Xs))
ll_2_in_ag₁([]_0) -> ll_2_out_ag₁(0_0)
ll_2_in_ga₁(s_1₁(N)) -> if_ll_2_in_1_ga₁(ll_2_in_ga₁(N))
ll_2_in_ga₁(0_0) -> ll_2_out_ga₁([]_0)
if_select_3_in_1_aga₁(select_3_out_aga₁(Ys)) -> select_3_out_aga₁(._2₁(Ys))
if_ll_2_in_1_ag₁(ll_2_out_ag₁(N)) -> ll_2_out_ag₁(s_1₁(N))
if_ll_2_in_1_ga₁(ll_2_out_ga₁(Xs)) -> ll_2_out_ga₁(._2₁(Xs))

The set Q consists of the following terms:

select_3_in_aga₁(x0)
ll_2_in_ag₁(x0)
ll_2_in_ga₁(x0)
if_select_3_in_1_aga₁(x0)
if_ll_2_in_1_ag₁(x0)
if_ll_2_in_1_ga₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_T_1_IN_2_G₁, IF_T_1_IN_1_G₁, IF_T_1_IN_3_G₁, T_1_IN_G₁}.
By using a polynomial ordering, the following set of Dependency Pairs of this DP problem can be strictly oriented.

IF_T_1_IN_2_G₁(select_3_out_aga₁(Xs1)) -> IF_T_1_IN_3_G₁(ll_2_in_ag₁(Xs1))

The remaining Dependency Pairs were at least non-strictly be oriented.

IF_T_1_IN_1_G₁(ll_2_out_ga₁(Xs)) -> IF_T_1_IN_2_G₁(select_3_in_aga₁(Xs))
IF_T_1_IN_3_G₁(ll_2_out_ag₁(M)) -> T_1_IN_G₁(M)
T_1_IN_G₁(N) -> IF_T_1_IN_1_G₁(ll_2_in_ga₁(N))

With the implicit AFS we had to orient the following set of usable rules non-strictly.

if_ll_2_in_1_ga₁(ll_2_out_ga₁(Xs)) -> ll_2_out_ga₁(._2₁(Xs))
if_select_3_in_1_aga₁(select_3_out_aga₁(Ys)) -> select_3_out_aga₁(._2₁(Ys))
ll_2_in_ag₁(._2₁(Xs)) -> if_ll_2_in_1_ag₁(ll_2_in_ag₁(Xs))
ll_2_in_ga₁(s_1₁(N)) -> if_ll_2_in_1_ga₁(ll_2_in_ga₁(N))
ll_2_in_ga₁(0_0) -> ll_2_out_ga₁([]_0)
if_ll_2_in_1_ag₁(ll_2_out_ag₁(N)) -> ll_2_out_ag₁(s_1₁(N))
select_3_in_aga₁(._2₁(Xs)) -> select_3_out_aga₁(Xs)
select_3_in_aga₁(._2₁(Xs)) -> if_select_3_in_1_aga₁(select_3_in_aga₁(Xs))
ll_2_in_ag₁([]_0) -> ll_2_out_ag₁(0_0)

Used ordering: POLO with Polynomial interpretation:

POL(0_0) = 0
POL(if_ll_2_in_1_ga₁(x₁)) = 1 + x₁
POL(if_select_3_in_1_aga₁(x₁)) = 1 + x₁
POL([]_0) = 0
POL(IF_T_1_IN_1_G₁(x₁)) = x₁
POL(ll_2_in_ag₁(x₁)) = x₁
POL(if_ll_2_in_1_ag₁(x₁)) = 1 + x₁
POL(ll_2_in_ga₁(x₁)) = x₁
POL(select_3_out_aga₁(x₁)) = 1 + x₁
POL(ll_2_out_ga₁(x₁)) = x₁
POL(IF_T_1_IN_3_G₁(x₁)) = x₁
POL(ll_2_out_ag₁(x₁)) = x₁
POL(T_1_IN_G₁(x₁)) = x₁
POL(IF_T_1_IN_2_G₁(x₁)) = x₁
POL(s_1₁(x₁)) = 1 + x₁
POL(select_3_in_aga₁(x₁)) = x₁
POL(._2₁(x₁)) = 1 + x₁

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPPoloProof

                          ↳ QDP

                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

IF_T_1_IN_1_G₁(ll_2_out_ga₁(Xs)) -> IF_T_1_IN_2_G₁(select_3_in_aga₁(Xs))
IF_T_1_IN_3_G₁(ll_2_out_ag₁(M)) -> T_1_IN_G₁(M)
T_1_IN_G₁(N) -> IF_T_1_IN_1_G₁(ll_2_in_ga₁(N))

The TRS R consists of the following rules:

select_3_in_aga₁(._2₁(Xs)) -> if_select_3_in_1_aga₁(select_3_in_aga₁(Xs))
select_3_in_aga₁(._2₁(Xs)) -> select_3_out_aga₁(Xs)
ll_2_in_ag₁(._2₁(Xs)) -> if_ll_2_in_1_ag₁(ll_2_in_ag₁(Xs))
ll_2_in_ag₁([]_0) -> ll_2_out_ag₁(0_0)
ll_2_in_ga₁(s_1₁(N)) -> if_ll_2_in_1_ga₁(ll_2_in_ga₁(N))
ll_2_in_ga₁(0_0) -> ll_2_out_ga₁([]_0)
if_select_3_in_1_aga₁(select_3_out_aga₁(Ys)) -> select_3_out_aga₁(._2₁(Ys))
if_ll_2_in_1_ag₁(ll_2_out_ag₁(N)) -> ll_2_out_ag₁(s_1₁(N))
if_ll_2_in_1_ga₁(ll_2_out_ga₁(Xs)) -> ll_2_out_ga₁(._2₁(Xs))

The set Q consists of the following terms:

select_3_in_aga₁(x0)
ll_2_in_ag₁(x0)
ll_2_in_ga₁(x0)
if_select_3_in_1_aga₁(x0)
if_ll_2_in_1_ag₁(x0)
if_ll_2_in_1_ga₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_T_1_IN_2_G₁, IF_T_1_IN_1_G₁, T_1_IN_G₁, IF_T_1_IN_3_G₁}.
The approximation of the Dependency Graph contains 0 SCCs with 3 less nodes.